Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
Q is empty.
↳ QTRS
↳ Overlay + Local Confluence
Q restricted rewrite system:
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
Q is empty.
The TRS is overlay and locally confluent. By [19] we can switch to innermost.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
The set Q consists of the following terms:
a(f, a(f, a(g, a(g, x0))))
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
A(f, a(f, a(g, a(g, x)))) → A(f, x)
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(f, a(f, a(f, x)))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(g, a(f, a(f, a(f, x))))
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(g, a(f, a(f, a(f, x))))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
The set Q consists of the following terms:
a(f, a(f, a(g, a(g, x0))))
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(f, a(f, a(g, a(g, x)))) → A(f, x)
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(f, a(f, a(f, x)))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(g, a(f, a(f, a(f, x))))
A(f, a(f, a(g, a(g, x)))) → A(g, a(g, a(g, a(f, a(f, a(f, x))))))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
The set Q consists of the following terms:
a(f, a(f, a(g, a(g, x0))))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ATransformationProof
Q DP problem:
The TRS P consists of the following rules:
A(f, a(f, a(g, a(g, x)))) → A(f, x)
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, x))
A(f, a(f, a(g, a(g, x)))) → A(f, a(f, a(f, x)))
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
The set Q consists of the following terms:
a(f, a(f, a(g, a(g, x0))))
We have to consider all minimal (P,Q,R)-chains.
We have applied the A-Transformation [17] to get from an applicative problem to a standard problem.
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ ATransformationProof
↳ QDP
↳ RFCMatchBoundsDPProof
Q DP problem:
The TRS P consists of the following rules:
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(x)
The TRS R consists of the following rules:
f(f(g(g(x)))) → g(g(g(f(f(f(x))))))
The set Q consists of the following terms:
f(f(g(g(x0))))
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 4.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(x)
To find matches we regarded all rules of R and P:
f(f(g(g(x)))) → g(g(g(f(f(f(x))))))
f1(f(g(g(x)))) → f1(f(f(x)))
f1(f(g(g(x)))) → f1(f(x))
f1(f(g(g(x)))) → f1(x)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
32, 33, 34, 35, 37, 36, 39, 40, 38, 42, 41, 44, 45, 43, 47, 46, 49, 50, 48, 52, 51, 54, 55, 53, 57, 56, 59, 60, 58, 62, 61, 67, 66, 65, 64, 63
Node 32 is start node and node 33 is final node.
Those nodes are connect through the following edges:
- 32 to 34 labelled f1_1(0)
- 32 to 35 labelled f1_1(0)
- 32 to 33 labelled f1_1(0), f1_1(1)
- 32 to 36 labelled f1_1(1)
- 32 to 37 labelled f1_1(1)
- 32 to 39 labelled f1_1(1), f1_1(2)
- 32 to 46 labelled f1_1(2)
- 32 to 47 labelled f1_1(2)
- 32 to 51 labelled f1_1(2)
- 32 to 52 labelled f1_1(2)
- 32 to 43 labelled f1_1(2)
- 32 to 56 labelled f1_1(3)
- 32 to 57 labelled f1_1(3)
- 32 to 45 labelled f1_1(3)
- 32 to 61 labelled f1_1(3)
- 32 to 62 labelled f1_1(3)
- 32 to 49 labelled f1_1(3)
- 32 to 66 labelled f1_1(4)
- 32 to 67 labelled f1_1(4)
- 32 to 59 labelled f1_1(4)
- 33 to 33 labelled #_1(0)
- 34 to 35 labelled f_1(0)
- 34 to 38 labelled g_1(1)
- 35 to 33 labelled f_1(0)
- 35 to 38 labelled g_1(1)
- 37 to 33 labelled f_1(1)
- 37 to 38 labelled g_1(1)
- 37 to 39 labelled f_1(1)
- 36 to 37 labelled f_1(1)
- 36 to 38 labelled g_1(1)
- 36 to 48 labelled g_1(2)
- 39 to 40 labelled g_1(1)
- 40 to 41 labelled f_1(1)
- 40 to 43 labelled g_1(2)
- 38 to 39 labelled g_1(1)
- 42 to 33 labelled f_1(1)
- 42 to 38 labelled g_1(1)
- 41 to 42 labelled f_1(1)
- 41 to 38 labelled g_1(1)
- 44 to 45 labelled g_1(2)
- 45 to 46 labelled f_1(2)
- 43 to 44 labelled g_1(2)
- 47 to 39 labelled f_1(2)
- 46 to 47 labelled f_1(2)
- 46 to 48 labelled g_1(2)
- 49 to 50 labelled g_1(2)
- 50 to 51 labelled f_1(2)
- 48 to 49 labelled g_1(2)
- 52 to 43 labelled f_1(2)
- 51 to 52 labelled f_1(2)
- 51 to 53 labelled g_1(3)
- 54 to 55 labelled g_1(3)
- 55 to 56 labelled f_1(3)
- 55 to 63 labelled g_1(4)
- 53 to 54 labelled g_1(3)
- 57 to 45 labelled f_1(3)
- 57 to 58 labelled g_1(3)
- 56 to 57 labelled f_1(3)
- 59 to 60 labelled g_1(3)
- 60 to 61 labelled f_1(3)
- 58 to 59 labelled g_1(3)
- 62 to 49 labelled f_1(3)
- 61 to 62 labelled f_1(3)
- 67 to 59 labelled f_1(4)
- 66 to 67 labelled f_1(4)
- 65 to 66 labelled f_1(4)
- 64 to 65 labelled g_1(4)
- 63 to 64 labelled g_1(4)